package ch.epfl.lara.matcheck.ast;

import ch.epfl.lara.matcheck.ast._

import scala.util.parsing.input.Positional


abstract class Trees extends Positional         
  
sealed abstract class Tree extends Trees
    
final case class Program(constraint: Option[Formula], 
    			 domain: Option[Formula],
                         objects: List[ObjectDef], 
                         classes: List[ClassDef]) 
  extends Tree 


// -------------------------- Top Level --------------------------

trait TopDecl {
  def inv: Option[Formula]
}
  
final case class ObjectDef(name: Name[ObjectSymbol], 
                           invariant: Option[Formula], 
                           methods: List[MethodDef]) 
  extends Tree with TopDecl {
  def getName: String = name.getName
  def inv = this.invariant
  def isMain: Boolean = methods.exists(_.getName == "main")
  def isExtractor: Boolean = methods.exists(_.getName == Constants.UNAPPLY)
  
  def getUnapply: MethodDef = { 
    if(isExtractor) methods.find(_.getName == Constants.UNAPPLY).get
    else throw new Exception("object "+name+" is not an extractor")
  }
  
  def getMain: Option[MethodDef] =
    methods.find(_.getName == "main")
	
  
  def getUnapplyParamTypeName: String = 
    getUnapply.params.head.tpe.toString
}
    

final case class ClassDef(isSealed: Boolean,
                          isAbstract: Boolean, 
                          name: Name[ClassSymbol], 
                          fields: List[FieldDef], 
                          superclass: Option[String], 
                          invariant: Option[Formula], 
                          methods: List[MethodDef]) 
  extends Tree with TopDecl  {
   
    def getName: String = name.getName
    def getSymbol: ClassSymbol = name.sym
    def inv = invariant
  }


// -------------------------- Members --------------------------

sealed abstract class Members extends Tree 
  
final case class FieldDef(name: Name[FieldSymbol], tpe: TypeTree) extends Members {
  def getName: String = name.getName
}
  
final case class ParamDef(name: Name[VarSymbol], tpe: TypeTree) extends Tree {
  def getName: String = name.getName
  def getTpe: String = tpe.toString
}

    
final case class MethodDef(name: Name[MethodSymbol], 
                           params: List[ParamDef], 
                           returnTpe: TypeTree, 
                           ppc: Option[(Formula,Formula)],
                           body: Expr) 
  extends Members {
    val self: String = "this";
    
    def getName: String = name.getName
    def getContainerSym: Symbol = name.getSym.getSym 
  }


//-------------------------- Expression --------------------------

sealed abstract class Expr extends Tree 

trait PatternMatching 

final case class Match(scrutinee: Expr, 
                       tpe: TypeTree, 
                       cases: List[CaseDef]) 
  extends Expr with PatternMatching {
     
    /**
     * Retrieve the list of pattern declaration of the current match expression
     */
    def getPatterns: List[PatternDef] = 
      for(val CaseDef(_,pattern,_,_) <- cases) yield pattern
       
  }

final case class CaseDef(position: Int, 
                         pattern: PatternDef, 
                         guard: Option[Expr], 
                         body: Expr) 
  extends Tree with PatternMatching


sealed abstract class PatternDef extends Tree with PatternMatching 

final case class VarPattern(name: Name[LocalSymbol], tpe: TypeTree) extends PatternDef

final case class ClassPattern(objname: Name[ObjectSymbol], 
                              args: List[PatternDef]) 
  extends PatternDef
  
final case object Wildcard extends PatternDef


final case class Ident(name: Name[VarSymbol]) extends Expr 
final case class ObjectId(name: Name[ObjectSymbol]) extends Expr
final case object True extends Expr 
final case object False extends Expr 
final case class Call(obj: Expr, method: Name[MethodSymbol], args: List[Expr]) extends Expr  
final case class Select(obj: Expr, field: Name[FieldSymbol]) extends Expr 
final case class If(cond: Expr, then: Expr, elze: Expr) extends Expr 
final case class New(name: Name[ClassSymbol], args: List[Expr]) extends Expr 
final case class IsInstanceOf(e: Expr, tpe: TypeTree) extends Expr 
    

final case class StringLit(lit: String) extends Expr 
final case class Number(n: Int) extends Expr 

abstract class Operator extends Expr 
final case class +(left: Expr, right: Expr) extends Operator
final case class -(left: Expr, right: Expr) extends Operator
final case class *(left: Expr, right: Expr) extends Operator 
final case class /(left: Expr, right: Expr) extends Operator
final case class %(left: Expr, right: Expr) extends Operator
final case class ==(left: Expr, right: Expr) extends Operator
final case class <(left: Expr, right: Expr) extends Operator
final case class <=(left: Expr, right: Expr) extends Operator
final case class &&(left: Expr, right: Expr) extends Operator
final case class ||(left: Expr, right: Expr) extends Operator
final case class !(e: Expr) extends Operator
// Internally used
final case class ->(left: Expr, right: Expr) extends Operator
	
	
// -------------------------- Type Tree --------------------------

sealed abstract class TypeTree extends Tree {
  def isPredefinedType = true 
}
 
final case class ClassType(c: String) extends TypeTree {
  override def isPredefinedType = false
  override def toString = c
}

final case class OptionType(seq: List[TypeTree]) extends TypeTree {
  override def toString =  
    "OptionOf" + 
      ( if (seq.length > 1) seq.map(_.toString).mkString("")
          else seq.head )         
}

/**final case class ListType(tpe: TypeTree) extends TypeTree {
  override def toString = "ListOf" + tpe + ""
}*/

final case class ParamType(tpe: TypeTree, ptpe: TypeTree) extends TypeTree {
  override def toString = tpe+"Of" + ptpe + ""
}  
  
final case object IntType extends TypeTree with Predefined {
  override def toString = INT_SET
}

final case object BoolType extends TypeTree with Predefined {
  override def toString = BOOL_SET
}